#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "klee_change_macros.h"
#include "klee_change_functions.h"
/*
 * Yi's example in klee
 */

int lib(int x){
	if (x > klee_change(11,10))
		return 11;
	else
		return klee_change(x-1,x);
}

int client(int x){
	if (x > lib(x))
		return x;
	else
		return lib(x);
}

int main(int argc, char *argv[]) {
  int x= argv[1][0] - '0';
  return client(x);
}
